$\forall$$P$:(chain\_config()$\rightarrow\mathbb{P}$).
\\[0ex]$P$(cchead())
\\[0ex]$\Rightarrow$ $P$(cctail())
\\[0ex]$\Rightarrow$ ($\forall$${\it id}$:Id. $P$(ccpred(${\it id}$)))
\\[0ex]$\Rightarrow$ ($\forall$${\it id}$:Id, ${\it num}$:$\mathbb{N}$. $P$(ccsucc(${\it id}$;${\it num}$)))
\\[0ex]$\Rightarrow$ \{$\forall$$x$:chain\_config(). $P$($x$)\}